Nuprl Lemma : f2f+-p+-field 11,40
es:ES, ff:FIFO, f2f+:F2F+-decls, sndr, rcvr:ff.C, e, e':E.
(f2f+-p+(e,e'))
 {([e: sndr is_req   rcvr]  [e: rcvr is_ack  sndr])
 & ([e': sndr is_req   rcvr]  [e': rcvr is_ack  sndr])} 
latex

Definitions{T}, A c B, , P  Q, P & Q, t  T, P  Q, x:A. B(x), f2f+-p+
Lemmasf2f+-pred-field, f2f+Ack wf, f2f+Req wf, snd-it wf, f2f+-pred wf, rel plus field, event system wf, FIFO wf, F2F+-decls wf, fifoC wf, es-E wf, f2f+-p+ wf

origin